Concurrency with synchronization introduces new challenges to verification and testing, because some defects may only occur under specific interleaving of execution flows. This nondeterministic feature is due to the variety of possible execution orders in which tasks from different parallel processes may be scheduled. Model checking is a formal verification technique performing exhaustive state-space exploration. Given a system model, model checking can automatically check whether the model satisfies certain properties. In order to avoid favoring any particular execution order, the model checker interleaves operations in all possible ways, which may result in searching an exponentially large space of state transitions.
Dynamic Partial Order Reduction (DPOR) can reduce the size of state space by removing unnecessary state transitions. The core part of DPOR is determining independent concurrent operations, which requires building a happens-before relation based on a timestamp calculation for each operation. Most timestamp solutions require massive memory space at runtime. Some timestamp compression techniques aim to reduce the communication cost among processes in low-level message-passing systems, but these techniques cannot be directly applied to high-level synchronizations, such as Remote Procedure Call (RPC) and barriers. Many model checking tools also include internal state space compression capabilities. However, these compression capabilities barely consider the characteristics of timestamp structures and thus the compressed state cannot be easily reversed to determine causality relations among concurrent operations.